$\forall$$T$:Type, ${\it as}$, ${\it bs}$:$T$ List. sublist$\ast$($T$;${\it as}$;${\it bs}$) $\in$ Prop